b:. (b ~ tt)  (b ~ ff) 

latex

ProofTree

Definitions	t  T, x:A. B(x), ff, tt, P  Q, Unit, ,
Lemmas	bool wf